$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]single{-}thread{-}generator\{i:l\}(${\it es}$;$P$;$R$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. ($R$($e$,${\it e'}$)) $\Rightarrow$ ($P$($e$) \& $P$(${\it e'}$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$, $a$:E. $P$($e$) $\Rightarrow$ $P$($a$) $\Rightarrow$ ($e$ $<$ $a$) $\Rightarrow$ ($\exists$$m$:E. ($P$($m$) \& $R$($e$,$m$) \& ($R$$^{\mbox{\scriptsize $\ast$}}$)($m$,$a$))))